T:Type, L:(T List), P:({x:T| (x  L)} prop{i:l}). l-all(L; x.P(x))  prop{i:l} 

latex

Definitions	t  T, prop{i:l}, x:A. B(x), (x  l), guard(T), P  Q, P  Q, P  Q, P  Q, P  Q, x(s), x. t(x), l-all(L; x.P(x)), True
Lemmas	true wf, cons member, l member wf